T:(IdType), tab:secret-table(T). isl(next(tab))  ptr(tab)  ||tab||  

latex

Definitions	true, t  T, False, P  Q, isl(x), , A, AB, , {x:A| B(x) }, , inl(x), x:A. B(x), b, x:AB(x), a<b, #$n, x:AB(x), P & Q, i  j < k, {i..j}, false, Type, Prop, True, ij, b, s = t, i<j, T, P  Q, P  Q, Unit, left+right, data(T), Atom$n, Id, ptr(tab), ||tab|| , next(tab), secret-table(T)
Lemmas	Id wf, int seg wf, nat wf, data wf, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, lt int wf, bool wf, bnot wf, le int wf, le wf, assert wf, false wf, btrue wf